DECLARE INDVAR x y x1 x2 y1 y2 z;
DECLARE PREDCONST atom 1;
DECLARE OPCONST cons 2;
DECLARE OPCONST car cdr 1;

axiom cons:
	∀x1 x2 y1 y2.(cons(x1,y1) = cons(x2,y2) ⊃ x1=x2 ∧ y1=y2),
	∀z.(¬atom(z) ≡ ∃x y.(z = cons(x,y))),
	∀x y. car(cons(x,y)) = x,
	∀x y. cdr(cons(x,y)) = y;;